/*@ nullable_by_default @*/
public class Test_Case{
    private /*@ spec_public @*/String [] tc;
    
    // A test case can include null pointers.
    // Therefore, there is no invariant on it.

    //@ requires size >= 0;
    //@ ensures tc.length == size;
    public Test_Case(int size){
	tc = new String[size];
    }

    // Adds s to the first null location.
    //@ requires s != null;
    //@ requires !full_tc();
    //@ ensures tc[\old(first_null())].equals(s);
    /*@ ensures (\forall int i; 0 <= i && i < tc.length; 
      @               i != \old(first_null()) ==> tc[i] == \old(tc[i]));
      @*/
    public void add(String s){
	tc[first_null()] = s;
    }

    //@ ensures  \result == tc.length;
    public /*@ pure @*/ int get_length(){
	return tc.length;
    }
    
    //@ requires 0<= i && i < tc.length;
    //@ ensures \result == tc[i];
    public /*@ pure @*/ String get_tc(int i){
	return tc[i];
    }

    // Adds s to location loc.
    //@ requires s != null;
    //@ requires loc >= 0 && loc < tc.length;
    //@ ensures tc[loc].equals(s);
    //@ ensures (\forall int i; 0 <= i && i < tc.length; i != loc ==> tc[i] == \old(tc[i]));
    // the last postcondition exploits the fact that a string is not mutable.
    public void add(String s, int loc){
	tc[loc] = s;
    }

    // returns the first null location
    //@ requires !full_tc();
    //@ ensures tc[\result] == null;
    //@ ensures (\forall int i; 0 <= i && i < \result; tc[i] != null);
    public /*@ pure @*/ int first_null(){
	int loc = -1;;
	for (int i = 0; i < tc.length; i++){
	    if (loc == -1 && tc[i] == null){loc = i;}
	}
	return loc;
    }

    // returns true if all locations are not null
    //@ ensures \result <==> (\forall int i; 0 <= i && i < tc.length; tc[i] != null);
    public /*@ pure @*/ boolean full_tc(){
	boolean full = true;
	for (int i = 0; i < tc.length; i++){
	    if (tc[i] == null){full = false;}
	}
	return full;
    }

    // returns true if the testcase have the same length and include the same strings.
    /*@ ensures
      @ \result <==>
      @ tc2 != null &&
      @ (tc.length == tc2.get_length()) &&
      @ (\forall int i; 0<= i && i<tc.length; 
      @               (tc[i] == null ==> tc2.get_tc(i) == null)
      @               && (tc[i] != null ==> tc[i].equals(tc2.get_tc(i))));
      @*/
    public /*@ pure @*/ boolean equals(Test_Case tc2){
	boolean result = true;
	if (tc2 == null){ result = false; }
	else if (tc2.get_length() != tc.length){ result = false; }
	else {for (int i = 0; i < tc.length; i++){
	           if (tc[i] == null && tc2.get_tc(i)!=null){result = false;};
	           if (!tc[i].equals(tc2.get_tc(i))) {result = false;}
	}}
		   return result;
    }
}
